Obtaining satisfactory coverage of modern, industry-scale software during testing is a highly challenging. For this, a testing agent typically is used to synthesize payloads that traverse possible execution paths identified in a static analysis. One way of accomplishing this is known as concolic execution. Concolic execution is a hybrid software verification technique that interleaves concrete execution (testing on particular inputs) with symbolic execution, a classical technique that treats program variables as symbolic variables. Symbolic execution is used in conjunction with an automated theorem prover or constraint solver based on constraint logic programming to generate new concrete inputs (test cases) with the aim of maximizing code coverage. With concolic execution, for example, a subject application can be instrumented so that that branching decisions made during the processing of a payload become visible to a testing component. In illustration, if there is a point during the application's run where the comparison “name!=‘John’” is performed, where “name” is a user-provided parameter, and the execution branches into the true branch of this test, then a next payload can set name to “John” to explore another execution path (e.g., where the false branch is followed). In this regard, the main focus of concolic execution is finding bugs in real-world software, rather than demonstrating program correctness.